\begin{tabbing}
$\vdash$  \=$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).\+
\\[0ex]($\forall$$a$, $b$:$T$. Dec($R$($a$,$b$)))
\\[0ex]$\Rightarrow$ \=(Connex($T$;$x$,$y$.$R$($x$,$y$))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=\{$\forall$$a$, $b$:$T$.\+
\\[0ex]strict\_part($x$,$y$.$R$($x$,$y$);$a$;$b$)
\\[0ex]$\vee$ Symmetrize($x$,$y$.$R$($x$,$y$);$a$;$b$)
\\[0ex]$\vee$ strict\_part($x$,$y$.$R$($x$,$y$);$b$;$a$)\})
\-\-\-
\end{tabbing}